Suchergebnisse

Norway has used e-voting in its last political election in September 2011, with more than 25 000 voters using the e-voting option. The underlying protocol is a new protocol designed by the ERGO group, involving several actors (a bulletin box but also a receipt generator, a decryption service, and an auditor). Of course, trusting the correctness and security of e-voting protocols is crucial in that context. Formal definitions of properties such as privacy, coercion-resistance or verifiability have been recently proposed, based on equivalence properties. In this paper, we propose a formal analysis of the protocol used in Norway, w.r.t. privacy, consid- ering several corruption scenarios. Part of this study has conducted using the ProVerif tool, on a simplified model. ; En Septembre 2011, la Norvège a mis en place le vote élec- tronique lors de ses élections politiques, avec plus de 25 000 votants qui ont effectivement utilisé cette option. Le protocole sous-jacent, créé par la com- pagnie ERGOgroup, met en jeu plusieurs acteurs (une urne mais également un générateur de reçu, un déchiffreur et un auditeur). Pouvoir faire confiance en l'exactitude et la sécurité des protocoles de votes électroniques est bien entendu crucial dans ce contexte. En se basant sur des propriétés d'équivalence, des définitions formelles de la confidentialité, de la résistance à la coercition ou de la vérifiabilité on été récemment proposées. Dans ce rapport, nous proposons une analyse formelle du protocole utilisé en Norvège dans le but de démontrer la propriété de confidentialité en considérant plusieurs scénarios de corruption. Une partie de cette étude a été menée avec l'utilisation de l'outil ProVerif, sur un modèle simplifié.

Norway has used e-voting in its last political election in September 2011, with more than 25 000 voters using the e-voting option. The underlying protocol is a new protocol designed by the ERGO group, involving several actors (a bulletin box but also a receipt generator, a decryption service, and an auditor). Of course, trusting the correctness and security of e-voting protocols is crucial in that context. Formal definitions of properties such as privacy, coercion-resistance or verifiability have been recently proposed, based on equivalence properties. In this paper, we propose a formal analysis of the protocol used in Norway, w.r.t. privacy, consid- ering several corruption scenarios. Part of this study has conducted using the ProVerif tool, on a simplified model. ; En Septembre 2011, la Norvège a mis en place le vote élec- tronique lors de ses élections politiques, avec plus de 25 000 votants qui ont effectivement utilisé cette option. Le protocole sous-jacent, créé par la com- pagnie ERGOgroup, met en jeu plusieurs acteurs (une urne mais également un générateur de reçu, un déchiffreur et un auditeur). Pouvoir faire confiance en l'exactitude et la sécurité des protocoles de votes électroniques est bien entendu crucial dans ce contexte. En se basant sur des propriétés d'équivalence, des définitions formelles de la confidentialité, de la résistance à la coercition ou de la vérifiabilité on été récemment proposées. Dans ce rapport, nous proposons une analyse formelle du protocole utilisé en Norvège dans le but de démontrer la propriété de confidentialité en considérant plusieurs scénarios de corruption. Une partie de cette étude a été menée avec l'utilisation de l'outil ProVerif, sur un modèle simplifié.

Norway has used e-voting in its last political election in September 2011, with more than 25 000 voters using the e-voting option. The underlying protocol is a new protocol designed by the ERGO group, involving several actors (a bulletin box but also a receipt generator, a decryption service, and an auditor). Of course, trusting the correctness and security of e-voting protocols is crucial in that context. Formal definitions of properties such as privacy, coercion-resistance or verifiability have been recently proposed, based on equivalence properties. In this paper, we propose a formal analysis of the protocol used in Norway, w.r.t. privacy, consid- ering several corruption scenarios. Part of this study has conducted using the ProVerif tool, on a simplified model. ; En Septembre 2011, la Norvège a mis en place le vote élec- tronique lors de ses élections politiques, avec plus de 25 000 votants qui ont effectivement utilisé cette option. Le protocole sous-jacent, créé par la com- pagnie ERGOgroup, met en jeu plusieurs acteurs (une urne mais également un générateur de reçu, un déchiffreur et un auditeur). Pouvoir faire confiance en l'exactitude et la sécurité des protocoles de votes électroniques est bien entendu crucial dans ce contexte. En se basant sur des propriétés d'équivalence, des définitions formelles de la confidentialité, de la résistance à la coercition ou de la vérifiabilité on été récemment proposées. Dans ce rapport, nous proposons une analyse formelle du protocole utilisé en Norvège dans le but de démontrer la propriété de confidentialité en considérant plusieurs scénarios de corruption. Une partie de cette étude a été menée avec l'utilisation de l'outil ProVerif, sur un modèle simplifié.

The SwissPost e-voting system is currently proposed under the scrutiny of the community, before being deployed in 2022 for political elections in several Swiss Cantons. We explain how real world constraints led to shortcomings that allowed a privacy attack to be mounted. More precisely, dishonest authorities can learn the vote of several voters of their choice, without being detected, even when the requested threshold of honest authorities act as prescribed.

The SwissPost e-voting system is currently proposed under the scrutiny of the community, before being deployed in 2022 for political elections in several Swiss Cantons. We explain how real world constraints led to shortcomings that allowed a privacy attack to be mounted. More precisely, dishonest authorities can learn the vote of several voters of their choice, without being detected, even when the requested threshold of honest authorities act as prescribed.

Electronic voting systems aim at two conflicting properties, namely privacy and verifiability, while trying to minimise the trust assumptions on the various voting components. Most existing voting systems either assume trust in the voting device or in the voting server. We propose a novel remote voting scheme BeleniosVS that achieves both privacy and verifiability against a dishonest voting server as well as a dishonest voting device. In particular, a voter does not leak her vote to her voting device and she can check that her ballot on the bulletin board does correspond to her intended vote. More specifically, we assume two elections authorities: the voting server and a registrar that acts only during the setup. Then BeleniosVS guarantees both privacy and verifiability against a dishonest voting device, provided that not both election authorities are corrupted. Additionally, our scheme guarantees receipt-freeness against an external adversary. We provide a formal proof of privacy, receipt-freeness, and verifiability using the tool ProVerif, covering a hundred cases of threat scenarios. Proving verifiability required to develop a set of sufficient conditions, that can be handled by ProVerif. This contribution is of independent interest.

Electronic voting systems aim at two conflicting properties, namely privacy and verifiability, while trying to minimise the trust assumptions on the various voting components. Most existing voting systems either assume trust in the voting device or in the voting server. We propose a novel remote voting scheme BeleniosVS that achieves both privacy and verifiability against a dishonest voting server as well as a dishonest voting device. In particular, a voter does not leak her vote to her voting device and she can check that her ballot on the bulletin board does correspond to her intended vote. More specifically, we assume two elections authorities: the voting server and a registrar that acts only during the setup. Then BeleniosVS guarantees both privacy and verifiability against a dishonest voting device, provided that not both election authorities are corrupted. Additionally, our scheme guarantees receipt-freeness against an external adversary. We provide a formal proof of privacy, receipt-freeness, and verifiability using the tool ProVerif, covering a hundred cases of threat scenarios. Proving verifiability required to develop a set of sufficient conditions, that can be handled by ProVerif. This contribution is of independent interest.

International audience ; Electronic voting systems aim at two conflicting properties, namely privacy and verifiability, while trying to minimise the trust assumptions on the various voting components. Most existing voting systems either assume trust in the voting device or in the voting server. We propose a novel remote voting scheme BeleniosVS that achieves both privacy and verifiability against a dishonest voting server as well as a dishonest voting device. In particular, a voter does not leak her vote to her voting device and she can check that her ballot on the bulletin board does correspond to her intended vote. More specifically, we assume two elections authorities: the voting server and a registrar that acts only during the setup. Then BeleniosVS guarantees both privacy and verifiability against a dishonest voting device, provided that not both election authorities are corrupted. Additionally, our scheme guarantees receipt-freeness against an external adversary. We provide a formal proof of privacy, receipt-freeness, and verifiability using the tool ProVerif, covering a hundred cases of threat scenarios. Proving verifiability required to develop a set of sufficient conditions, that can be handled by ProVerif. This contribution is of independent interest.

International audience ; Electronic voting systems aim at two conflicting properties, namely privacy and verifiability, while trying to minimise the trust assumptions on the various voting components. Most existing voting systems either assume trust in the voting device or in the voting server. We propose a novel remote voting scheme BeleniosVS that achieves both privacy and verifiability against a dishonest voting server as well as a dishonest voting device. In particular, a voter does not leak her vote to her voting device and she can check that her ballot on the bulletin board does correspond to her intended vote. More specifically, we assume two elections authorities: the voting server and a registrar that acts only during the setup. Then BeleniosVS guarantees both privacy and verifiability against a dishonest voting device, provided that not both election authorities are corrupted. Additionally, our scheme guarantees receipt-freeness against an external adversary. We provide a formal proof of privacy, receipt-freeness, and verifiability using the tool ProVerif, covering a hundred cases of threat scenarios. Proving verifiability required to develop a set of sufficient conditions, that can be handled by ProVerif. This contribution is of independent interest.

International audience ; Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously. In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and verifiability properties. Our analysis mostly confirms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast verifiability, even if the voter's device is compromised. To our knowledge, this is the first time a full-fledged automatic symbolic analysis of an e-voting system used for politically-binding elections has been realized.

International audience ; Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously. In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and verifiability properties. Our analysis mostly confirms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast verifiability, even if the voter's device is compromised. To our knowledge, this is the first time a full-fledged automatic symbolic analysis of an e-voting system used for politically-binding elections has been realized.

Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously. In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and veri-fiability properties. Our analysis mostly confirms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast verifiability, even if the voter's device is compromised. To our knowledge, this is the first time a full-fledged automatic symbolic analysis of an e-voting system used for politically-binding elections has been realized.

Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously. In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and veri-fiability properties. Our analysis mostly confirms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast verifiability, even if the voter's device is compromised. To our knowledge, this is the first time a full-fledged automatic symbolic analysis of an e-voting system used for politically-binding elections has been realized.

While extensive research addresses the problem of establishing session keys through cryptographic protocols, relatively little work has appeared addressing the problem of revocation and update of long term keys. We present an API for symmetric key management on embedded devices that supports revocation and prove security properties design in the symbolic model of cryptography. Our API supports two modes of revocation: a passive mode where keys have an expiration time, and an active mode where revocation messages are sent to devices. For the first we show that once enough time has elapsed after the compromise of a key, the system returns to a secure state, i.e. the API is robust against attempts by the attacker to use a compromised key to compromise other keys or keep the compromised key alive past its validity time. For the second we show that once revocation messages have been received the system is immediately in a secure state. Notable features of our designs are that all secret values on the device are revocable, and the device returns to a functionally equivalent state after revocation is complete. ; De nombreuses recherches traitent du problème de l'établissement de clefs de session à l'aide de protocoles cryptographiques. Inversement, il y a eu relativement peu de travaux concernant le problème de la révocation et la mise à jour de clefs à longue durée de vie. Nous présentons une API, pour la gestion de clefs symétriques sur des systèmes embarqués, qui supporte la révocation et nous démontrons ses propriétés de sécurité dans le modèle symbolique. Notre API permet deux modes de révocation : le premier, passif, se base sur une durée de vie limitée attribuée aux clefs et le second, actif, envoie des instructions de révocation de clef aux différents dispositifs. Notre premier résultat démontre que, lorsqu'une clef est compromise, le système retourne, après un certain temps, dans un état sécurisé, c.à.d. un état où les API's respectent la politique de sécurité. Le second résultat montre, qu'une fois les messages de révocation réceptionnés, les appareils retournent immédiatement dans un état sécurisé. Les particularités principales de notre schéma sont que tous les secrets contenus dans un appareil sont révocables et, qu'après révocation, l'appareil retourne dans un état fonctionnel.

While extensive research addresses the problem of establishing session keys through cryptographic protocols, relatively little work has appeared addressing the problem of revocation and update of long term keys. We present an API for symmetric key management on embedded devices that supports revocation and prove security properties design in the symbolic model of cryptography. Our API supports two modes of revocation: a passive mode where keys have an expiration time, and an active mode where revocation messages are sent to devices. For the first we show that once enough time has elapsed after the compromise of a key, the system returns to a secure state, i.e. the API is robust against attempts by the attacker to use a compromised key to compromise other keys or keep the compromised key alive past its validity time. For the second we show that once revocation messages have been received the system is immediately in a secure state. Notable features of our designs are that all secret values on the device are revocable, and the device returns to a functionally equivalent state after revocation is complete. ; De nombreuses recherches traitent du problème de l'établissement de clefs de session à l'aide de protocoles cryptographiques. Inversement, il y a eu relativement peu de travaux concernant le problème de la révocation et la mise à jour de clefs à longue durée de vie. Nous présentons une API, pour la gestion de clefs symétriques sur des systèmes embarqués, qui supporte la révocation et nous démontrons ses propriétés de sécurité dans le modèle symbolique. Notre API permet deux modes de révocation : le premier, passif, se base sur une durée de vie limitée attribuée aux clefs et le second, actif, envoie des instructions de révocation de clef aux différents dispositifs. Notre premier résultat démontre que, lorsqu'une clef est compromise, le système retourne, après un certain temps, dans un état sécurisé, c.à.d. un état où les API's respectent la politique de sécurité. Le second ...